1. Field of the Invention
The present invention relates to a method and system for performing verification of logic circuits and a corresponding computer program product.
2. Description and Disadvantages of Prior Art
Digital logic circuits implement a logic function and represent the core of any computing processing unit. Thus, before a “logic design” is constructed in real hardware, it must be tested and the proper operation thereof has to be verified against a design specification. For example, this is done in prior art by simulating a so-called gate-level netlist. This gate-level netlist has a graph structure with Boolean gates as nets and nets as connecting arcs. Storage elements like latches can be built from Boolean gates and are commonly included as atomic latch instances in a gate-level netlist. In the following, we assume that a latch is included as an atomic latch instance in a gate-level netlist. Also, the abbreviated term “netlist” may be substituted for “gate-level netlist”. This gate-level netlist is representing the respective sections of the desired hardware circuit.
Assume, a simple exemplary digital circuit has a plurality of 16 input bits. Then, a plurality of 2 to the power of 16=65536 different input settings exist, which should be tested in total for correct operation of the circuit, or its logic model, respectively. This is already a time-consuming work, either done by a computer, but at least surveyed in critical points within the circuit by the hardware developer engineering team. Thus, this way of hardware verification is called “exhaustive” functional verification.
Today's hardware designs, however, are much more complex than the before-mentioned simple 16-bit circuit. Even single sections of a hardware design may comprise hundreds, or several thousands of input variables.
This enormous input bit setting space cannot be verified in such exhaustive way, covering for example a plurality of (2 exp 2500) different input settings, i.e. “stimuli”, and their correct propagation through the gate-level netlist. Thus, a so-called “biased, random” verification is done, selecting some bit settings only, the propagation of which seems to touch at least some of the “problematic zones” in a hardware design. Such selection might be to select an input bit pattern consisting of only “0”, one of only ‘1’, (corner cases), and some randomly selected patterns in-between them, comprising both values. There are also variations in that type of methods in prior art, like “walking 1s”, etc.
In summary, the drawbacks of exhaustive functional verification are: The simulation runtime is very long due to an exhaustive set of stimuli. In many cases it is a time-consuming task to check that all possible combinations for example on a certain data path in a gate-level netlist are exercised, and that they work correctly.
A full (complete) checking is difficult to perform, since a logic function does not necessarily generate signal level changes, when for example, only one bit is changed in relation to the preceding input bit pattern. This is due to restrictions in the testbench, when registers are being set and reset, but there are only special combinations allowed (i.e. writing zeros to a register that shows already only zeros).
An alternative for doing exhaustive, bit value oriented, functional simulation is the prior art “symbolic” simulation, as schematically depicted in FIG. 2. Here, instead of bit values, symbols are propagated through the gate-level netlist. For example, a 2-input AND gate with input symbols “a” and “b” produces a result “a AND b”. This short logic expression is then the input for another gate, thus, maybe “a AND b OR c” results after the next step in a selected path. A long path in the logic results in an expression of significant extent. If, further, some feedback loop connects between some net location and a preceding net location of the propagation path, such expression can easily “explode”. This is a disadvantageous limitation of symbolic simulation or verification.
In summary, the drawbacks of “symbolic simulation” are:
First, only small designs can be verified due to the possible expression explosion. Further, such expressions grow dynamically; therefore the simulation cannot be run on so-called hardware accelerators, i.e. on dedicated high-performance simulation servers. Further, as the symbols have no value, a regular, usual bit-value-based functional simulation cannot be carried out simultaneously, which is often strongly desired.
With reference to FIG. 1, prior art X-state simulation has only the anonymous indeterminate ‘X’, multi-value simulation may have more values between 0 and 1, for example ‘z’, but all of them are anonymous. For X-state simulation, either plain 0/1 values or an ‘X’ are present at the circuit nets. Two different nets may carry an ‘X’, but a decision to set one ‘X’ to 0 does not mean that the other ‘X’ is set to 0 also. One only knows from the simulation if an indeterminate value ‘X’ may have an influence to some net or not, see FIG. 1 for an example circuit simulated with exemplary values.
A further prior art approach is disclosed in a yet unpublished patent application U.S. Ser. No. 11/009,350 of the Applicant. In this patent application a so-called “Colored-bits” simulation is dealing with the specific (but not determined) value at selected locations inside the gate-level netlist and their propagation through this netlist by the simulator. A value 0 at net “n1” colored ‘a’ is in sync with a value 1 colored ‘a’ at another netlist location ‘n2’, i.e. if ‘n1’ would be 1, ‘n2’ would be 0.
By this colored-bits simulation, one can make sure that some colored values transported through the logic would have been transported also with other values in the same way. But as soon as two colored-values are involved in a logical function of the netlist and both have to be propagated on a single net, colored-bits simulation loose all advantages and can only propagate an anonymous crunched color, i.e. an indefinite or indeterminate color, which has lost its particular property to be exactly a single specific color.